1. Field of the Invention
This invention relates to automated, formal verification techniques for logical systems such as digital circuits or communication protocol systems. More specifically, the invention relates to algorithms for such formal verification which are based on applications of graph theory.
2. Description of the Problem
Asynchronous circuits and systems are becoming an increasingly important alternative to synchronous systems. The formal verification of these circuits and systems, however, has been given somewhat less attention than their synchronous counterparts. In addition, many aggressively designed synchronous circuits rely on two-sided timing assumptions which are difficult to verify. Formal verification is often accomplished using graph theory and analysis. A logical system can assume any of a fixed set of states. These states, and their relationship to one another, can be represented by a directed graph (digraph). Such a digraph is commonly called a state transition graph (STG).
For computer analysis, a digraph such as an STG can be represented using an explicit data structure such as an adjacency list or an adjacency matrix. The decomposition of the digraph can be done in linear time using a depth-first search. However, in many real applications, the size of the digraph can be too large for explicit algorithms to be practical. One promising alternative is to use an implicit data structure to represent the digraph, for example, a binary decision diagram (BDD). Binary decision diagrams are described in an article by R. E. Bryant, xe2x80x9cGraph-Based Algorithm for Boolean Function Manipulation,xe2x80x9d IEEE Transactions on Computers, August 1986, which is incorporated herein by reference. Using a BDD, a digraph can be decomposed by finding all strongly connected components (SCC""s) in the reachable state space of a finite state machine that characterizes the logical system being analyzed. Computerized algorithms that decompose a digraph in this way compute the transitive closure of the state transition relation of the machine and then compute all SCC""s simultaneously. In practice, despite the advantages of an implicit data structure such a BDD, computing the transitive closure is very computationally expensive in both processor time and memory, resulting in large amounts of money and time being spent on formal verification.
The present invention provides for efficient, cost-effective formal verification of logical circuits and systems using an implicit enumeration of strongly connected components that is much less computationally expensive than other known methods. Using the method of the invention, a digraph is recursively partitioned and decomposed using reachability analysis. The algorithm of the invention can be applied to partitions or legal blocks of the circuit or system being analyzed so that each one can be verified separately and hierarchically. Non-trivial, strongly connected components derived through the use of the invention can be compared to expected behavior of a circuit or system. Alternatively, the invention can be applied to detect so-called xe2x80x9cbad cyclesxe2x80x9d which are encountered in many formal verification problems.
According to the present invention, a design is verified by first deriving a state transition graph (STG) for the design. If the logical system which is sought to be verified is large and complex, the system is partitioned into smaller logical blocks, partitions, or designs, and the algorithm is executed against each one. In any case a state transition graph for the design is recursively decomposed to determine all nontrivial strongly connected components of the STG. Each strongly connected component (SCC) represents an infinite behavior of the design. Each infinite behavior can be compared to an expected behavior in order to validate the design. This comparison can be made manually, or by a computer implemented comparison algorithm. In one embodiment, the algorithm of the invention recursively decomposes the STG by determining a backward set for each node in the STG, and finding non-trivial SCC""s in the backward set. It is also possible to use forward sets, or a combination of forward and backward sets.
In another embodiment of the invention, formal verification may be extended by determining if any non-trivial SCC derived as described above represents a bad cycle indicating a problem with a design. This determination is made by finding out if a non-trivial SCC is not in any cycle set. In another embodiment, the determination is made by finding out if an SCC intersects compliment sets of all cycle sets. Either bad cycle algorithm can stop and prompt an operator or designer upon finding the first bad cycle. Alternatively, an algorithm may find all bad cycles and present these to the designer.
In example embodiments of the invention, computer software is used to implement many aspects of the invention. The software can be stored on a medium. The medium can be magnetic, such as a diskette, tape, or fixed disk, or optical, such as a CD-ROM or DVD-ROM. The software can also be stored in a semiconductor device. Additionally, the software can be supplied via the Internet or some other type of network. A workstation or computer system that typically runs the software includes a plurality of input/output devices and a processor. The software in combination with the computer system and any peripheral hardware forms the means to execute the method of the invention.